A, C:Type, B:(AType), eqa:EqDecider(A), eqc, eqc':EqDecider(C), r:(AC), f:a:A fp B(a), a:A.
Inj(A; C; r)  a  dom(f)  rename(r;f)(r(a)) = f(a)  B(a) 

latex

Definitions	x:A. B(x), x(s), P  Q, f(x), rename(r;f), 2of(t), 1of(t), t  T, x. t(x), x:A. B(x), P & Q, Prop, P  Q, P  Q, a:A fp B(a), x  dom(f), A & B, Inj(A; B; f)
Lemmas	hd-filter, eqof wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, inject wf, fpf wf, deq wf, l member wf, assert-deq-member, deq property, subtype rel self